package systemf;

/**
 * System F求值器
 * 实现call-by-value求值策略
 */
public class Evaluator {
    
    /**
     * 求值：将项规约到范式
     */
    public Term evaluate(Term term) {
        Term current = term;
        Term next;
        
        // 持续规约直到无法继续
        while ((next = reduce(current)) != null) {
            current = next;
        }
        
        return current;
    }
    
    /**
     * 单步规约
     * @return 规约后的项，如果无法规约则返回null
     */
    public Term reduce(Term term) {
        if (term instanceof Term.App) {
            Term.App app = (Term.App) term;
            
            // 如果函数是Lambda，进行β-规约
            if (app.getFunction() instanceof Term.Lambda) {
                Term.Lambda lambda = (Term.Lambda) app.getFunction();
                Term argValue = evaluate(app.getArgument()); // call-by-value
                return lambda.getBody().substitute(lambda.getVar(), argValue);
            }
            
            // 如果函数可以规约，先规约函数
            Term reducedFunc = reduce(app.getFunction());
            if (reducedFunc != null) {
                return new Term.App(reducedFunc, app.getArgument());
            }
            
            // 如果参数可以规约，先规约参数
            Term reducedArg = reduce(app.getArgument());
            if (reducedArg != null) {
                return new Term.App(app.getFunction(), reducedArg);
            }
        } else if (term instanceof Term.TypeApp) {
            Term.TypeApp typeApp = (Term.TypeApp) term;
            
            // 如果项是类型抽象，进行类型应用规约
            if (typeApp.getTerm() instanceof Term.TypeAbs) {
                Term.TypeAbs typeAbs = (Term.TypeAbs) typeApp.getTerm();
                return typeSubstitute(typeAbs.getBody(), typeAbs.getTypeVar(), typeApp.getType());
            }
            
            // 如果项可以规约，先规约项
            Term reducedTerm = reduce(typeApp.getTerm());
            if (reducedTerm != null) {
                return new Term.TypeApp(reducedTerm, typeApp.getType());
            }
        }
        
        return null; // 无法规约
    }
    
    /**
     * 类型替换：在项中将类型变量替换为类型
     * 这用于类型应用的规约
     */
    private Term typeSubstitute(Term term, String typeVar, Type replacement) {
        if (term instanceof Term.Var) {
            return term;
        } else if (term instanceof Term.Lambda) {
            Term.Lambda lambda = (Term.Lambda) term;
            return new Term.Lambda(
                lambda.getVar(),
                lambda.getType().substitute(typeVar, replacement),
                typeSubstitute(lambda.getBody(), typeVar, replacement)
            );
        } else if (term instanceof Term.App) {
            Term.App app = (Term.App) term;
            return new Term.App(
                typeSubstitute(app.getFunction(), typeVar, replacement),
                typeSubstitute(app.getArgument(), typeVar, replacement)
            );
        } else if (term instanceof Term.TypeAbs) {
            Term.TypeAbs typeAbs = (Term.TypeAbs) term;
            // 如果类型变量相同，不替换（避免捕获）
            if (typeAbs.getTypeVar().equals(typeVar)) {
                return term;
            }
            return new Term.TypeAbs(
                typeAbs.getTypeVar(),
                typeSubstitute(typeAbs.getBody(), typeVar, replacement)
            );
        } else if (term instanceof Term.TypeApp) {
            Term.TypeApp typeApp = (Term.TypeApp) term;
            return new Term.TypeApp(
                typeSubstitute(typeApp.getTerm(), typeVar, replacement),
                typeApp.getType().substitute(typeVar, replacement)
            );
        }
        return term;
    }
    
    /**
     * 检查项是否为值（范式）
     */
    public boolean isValue(Term term) {
        return term instanceof Term.Var ||
               term instanceof Term.Lambda ||
               term instanceof Term.TypeAbs;
    }
}

